import java.net.*;
import java.io.*;

public class MCMASParser
{
    public static void MCMASSlaveParser(MCMASServerData serverData, MCMASClientData clientData)
    {
        try
        {
            String line;
            String[] execstr = {"/usr/bin/time", "-p", "./mcmas", "-e", "5", "-bmc_slave", "-init_bdd_file",
                                            serverData.directory + serverData.seedState, serverData.isplFile };

            System.out.println(serverData.isplFile + " " + serverData.directory + serverData.seedState);
            Process p = Runtime.getRuntime().exec(execstr);
            p.waitFor();
            BufferedReader input = new BufferedReader(new InputStreamReader(p.getInputStream()));
            BufferedReader error = new BufferedReader(new InputStreamReader(p.getErrorStream()));
            
            line = input.readLine();
            while (!line.equals("**** EXPERIMENT 5 ****")) { line = input.readLine(); }

            line = input.readLine();

            line = input.readLine();
            if (line.equals("TRUE"))
                clientData.cexFound = false;
            else
                clientData.cexFound = true;

            line = input.readLine();
            clientData.memoryUsed = Integer.parseInt(line.substring("Memory consumed: ".length(), line.length()));

            line = input.readLine();
            clientData.statesExplored = Integer.parseInt(line.substring("Reachable states: ".length(), line.length()));

            while ((line = error.readLine()) != null && !(line.substring(0, "user".length())).equals("user")) {}

            line = line.substring("user ".length(), line.length());
            clientData.timeUsed = Double.parseDouble(line);
        }
        catch (Exception e)
        {
        }
    }

    public static boolean MCMASMasterParser(MCMASServerData serverData, MCMASClientData clientData)
    //public static void main(String args[])
    {
        /*
        MCMASServerData serverData;
        serverData = new MCMASServerData();
        MCMASClientData clientData;
        clientData = new MCMASClientData();
        */
        try
        {
            String line;
            String[] execstr = {"/usr/bin/time", "-p", "./mcmas", "-e", "5", "-one_shot", "1" , serverData.isplFile };

            for (String s : execstr)
                System.out.print(s + " ");
            Process p = Runtime.getRuntime().exec(execstr);
            p.waitFor();
            BufferedReader input = new BufferedReader(new InputStreamReader(p.getInputStream()));
            BufferedReader error = new BufferedReader(new InputStreamReader(p.getErrorStream()));
            {
                line = input.readLine();
                while (!line.equals("**** EXPERIMENT 5 ****")) { line = input.readLine(); }

                line = input.readLine();
                
                if (!line.equals("Generating seeds"))
                {
                    // When we get there Line == Verifcation complete
                    // This means we've either reached a fixed point before the seed state depth
                    // OR, We've found a CEX
                    // Basically, this means that we have no seeds

                    serverData = null;

                    line = input.readLine();
                    if (line.equals("TRUE"))
                        clientData.cexFound = false;
                    else
                        clientData.cexFound = true;

                    line = input.readLine();
                    clientData.memoryUsed = Integer.parseInt(line.substring("Memory consumed: ".length(), line.length()));

                    line = input.readLine();
                    clientData.statesExplored = Integer.parseInt(line.substring("Reachable states: ".length(), line.length()));
                    
                    while ((line = error.readLine()) != null && !(line.substring(0, "user".length())).equals("user")) {}

                    line = line.substring("user ".length(), line.length());
                    clientData.timeUsed = Double.parseDouble(line);

                    return false;
                }
                else
                {
                    line = input.readLine();
                    serverData.directory = line.substring("Temporary directory: ".length(), line.length());

                    line = input.readLine();
                    serverData.totalSeeds = Integer.parseInt(line.substring("Generated seeds: ".length(), line.length()));

                    line = input.readLine();
                    clientData.memoryUsed = Integer.parseInt(line.substring("Memory consumed: ".length(), line.length()));

                    line = input.readLine();
                    clientData.statesExplored = Integer.parseInt(line.substring("Reachable states: ".length(), line.length()));
                    
                    while ((line = error.readLine()) != null && !(line.substring(0, "user".length())).equals("user")) {}

                    line = line.substring("user ".length(), line.length());
                    clientData.timeUsed = Double.parseDouble(line);

                    return true;
                }

            }
        }
        catch (Exception err) 
        {
            err.printStackTrace();
        }

        return false;

    }
}

